1. Field
The embodiments discussed herein are directed to verification, and more particularly, verification and reachability analysis of hardware or software design using an organic approach.
2. Description of the Related Art
As development of complex hardware and software design increases, limitations of existing verification techniques are becoming more evident. Verification generally deals with checking whether a software and/or hardware design satisfies an expected requirement with respect to a particular specification or property. A common approach to verification is checking properties of the design. One such approach is unbounded model checking of invariant properties of a system, which is generally performed by conducting a reachability analysis. This approach is directed to finding all states reachable from an initial state and checking whether the invariant properties are satisfied in the reachable states. Reachability analysis is typically performed using transition relation based image computation. However, the unbounded model checking and other similar approaches experience the so-called state explosion problem, especially in representing large designs, because sizes of representations dealing with reached states become exponentially large. Moreover, due to the sizes of the representations, a large memory space is required to store the representations.
In addition to requiring use of a large memory space, typical techniques for computing valid state sets require all reachable states to be computed because full error detection coverage is required. Since all image computation sub-operations need to be completed before new states are extracted, these techniques do not enable analysis or verification during a single image computation. That is, each conjunction can only be performed after a preceding one is completed. Thus, there is no mechanism of extracting new states until all image computation is complete.
Typically, valid state sets are computed by performing extensive circuit simulations, since a property can be invalidated if an invalid state is detected during simulation. However, validating a property through simulation is not possible, since the set of valid states is typically too large to explicitly enumerate. Although typical digital circuit verification has been performed by extensive simulations, their performance is unsatisfactory because simulations do not provide full coverage and only check a small portion of possible stimulus, leaving bugs/problems undetected.
Generally, verification involves running one image computation method until all image computations are complete, checking results thereof, and if unsatisfied by the results, running a different method. These techniques do not provide an intelligent way of determining an optimal solution without having to expend resources for computation of all reachable states and analyzing results of the individual techniques. It is also impossible to specify a method that should be applied at a particular stage of verification since typical verification techniques are restricted to a particular method until completion of all image computations.
Although various verification techniques have been proposed, existing verification techniques do not provide a way of identifying an optimal solution to efficiently perform verification. Since the difference between a suboptimal method and one which is better suited can be in orders of magnitude or more, there is a need for a verification system and method that provides an optimal verification solution.